SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Predicative programming</title>

</head>

Predicative programming

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">Not to be confused with <a href="List_of_conspiracy_theories#Predictive_programming" title="List of conspiracy theories">List of conspiracy theories § Predictive programming</a>.</div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

Predicative programming is the original name of a formal method for program <a href="Specification_language" title="Specification language">specification</a> and <a href="Program_refinement" class="mw-redirect" title="Program refinement">refinement</a>, more recently called a Practical Theory of Programming, invented by <a href="Eric_Hehner" title="Eric Hehner">Eric Hehner</a>. The central idea is that each specification is a binary (<a href="Boolean_domain" title="Boolean domain">boolean</a>) expression that is true of acceptable computer behaviors and false of unacceptable behaviors. It follows that refinement is just <a href="Material_conditional" title="Material conditional">implication</a>. This is the simplest formal method, and the most general, applying to sequential, parallel, stand-alone, communicating, terminating, nonterminating, natural-time, real-time, deterministic, and <a href="Probabilistic" class="mw-redirect" title="Probabilistic">probabilistic</a> programs, and includes time and space bounds.

Commands in a <a href="Programming_language" title="Programming language">programming language</a> are considered to be a special case of specification—those specifications that are compilable. For example, if the program variables are <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle z}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle z}</annotation>

</semantics>

</math><img src="./bf368e72c009decd9b6686ee84a375632e11de98.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.088ex; height:1.676ex;" alt="{\displaystyle z}" loading="lazy">, the command <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">+1 is equivalent to the specification (binary expression) <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">+1 ∧ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y'}</annotation>

</semantics>

</math><img src="./3a535de94a2183d7130731eab8a83531d7c35c6b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.845ex; height:2.843ex;" alt="{\displaystyle y'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy"> ∧ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle z'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle z'}</annotation>

</semantics>

</math><img src="./7c017ef8616d0c836e4b2a88c40931333c38dd19.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.775ex; height:2.509ex;" alt="{\displaystyle z'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle z}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle z}</annotation>

</semantics>

</math><img src="./bf368e72c009decd9b6686ee84a375632e11de98.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.088ex; height:1.676ex;" alt="{\displaystyle z}" loading="lazy"> in which <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle z}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle z}</annotation>

</semantics>

</math><img src="./bf368e72c009decd9b6686ee84a375632e11de98.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.088ex; height:1.676ex;" alt="{\displaystyle z}" loading="lazy"> represent the values of the program variables before the assignment, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y'}</annotation>

</semantics>

</math><img src="./3a535de94a2183d7130731eab8a83531d7c35c6b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.845ex; height:2.843ex;" alt="{\displaystyle y'}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle z'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle z'}</annotation>

</semantics>

</math><img src="./7c017ef8616d0c836e4b2a88c40931333c38dd19.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.775ex; height:2.509ex;" alt="{\displaystyle z'}" loading="lazy"> represent the values of the program variables after the assignment. If the specification is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">, we easily prove (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">+1) ⇒ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">), which says that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">+1 implies, or refines, or implements <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">.

Loop proofs are greatly simplified. For example, if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> is an integer variable, to prove that

while <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">>0 do <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">–1 od

refines, or implements the specification <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">≥0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">=0, prove

if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">>0 then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">–1; (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">≥0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">=0) else <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ok}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ok}</annotation>

</semantics>

</math><img src="./2d04f30d0b16aabe50853ba8a9b6702abd3947d2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.339ex; height:2.176ex;" alt="{\displaystyle ok}" loading="lazy"> fi ⇒ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">≥0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">=0)

where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ok}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ok}</annotation>

</semantics>

</math><img src="./2d04f30d0b16aabe50853ba8a9b6702abd3947d2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.339ex; height:2.176ex;" alt="{\displaystyle ok}" loading="lazy"> = (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">) is the empty, or do-nothing command. There is no need for a <a href="Loop_invariant" title="Loop invariant">loop invariant</a> or <a href="Least_fixed_point" title="Least fixed point">least fixed point</a>. Loops with multiple intermediate shallow and deep exits work the same way. This simplified form of proof is possible because program commands and specifications can be mixed together meaningfully.

Execution time (upper bounds, lower bounds, exact time) can be proven the same way, just by introducing a time variable. To prove termination, prove the execution time is finite. To prove nontermination, prove the execution time is infinite. For example, if the time variable is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy">, and time is measured by counting iterations, then to prove that execution of the previous while-loop takes time <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> when <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> is initially nonnegative, and takes forever when <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> is initially negative, prove

if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">>0 then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">–1; <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy">:= <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy">+1; (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">≥0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t'}</annotation>

</semantics>

</math><img src="./a69b623f18f6b111645f0ec200b3271729fa99af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.524ex; height:2.509ex;" alt="{\displaystyle t'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy">+<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"><0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t'}</annotation>

</semantics>

</math><img src="./a69b623f18f6b111645f0ec200b3271729fa99af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.524ex; height:2.509ex;" alt="{\displaystyle t'}" loading="lazy">=∞) else <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ok}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ok}</annotation>

</semantics>

</math><img src="./2d04f30d0b16aabe50853ba8a9b6702abd3947d2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.339ex; height:2.176ex;" alt="{\displaystyle ok}" loading="lazy"> fi

⇒ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">≥0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t'}</annotation>

</semantics>

</math><img src="./a69b623f18f6b111645f0ec200b3271729fa99af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.524ex; height:2.509ex;" alt="{\displaystyle t'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy">+<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"><0 ⇒ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t'}</annotation>

</semantics>

</math><img src="./a69b623f18f6b111645f0ec200b3271729fa99af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.524ex; height:2.509ex;" alt="{\displaystyle t'}" loading="lazy">=∞)

where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ok}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ok}</annotation>

</semantics>

</math><img src="./2d04f30d0b16aabe50853ba8a9b6702abd3947d2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.339ex; height:2.176ex;" alt="{\displaystyle ok}" loading="lazy"> = (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x'}</annotation>

</semantics>

</math><img src="./0ac74959896052e160a5953102e4bc3850fe93b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.014ex; height:2.509ex;" alt="{\displaystyle x'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> ∧ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t'}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t'}</annotation>

</semantics>

</math><img src="./a69b623f18f6b111645f0ec200b3271729fa99af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.524ex; height:2.509ex;" alt="{\displaystyle t'}" loading="lazy">=<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy">).

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

</div>

<ul><li>E.C.R. Hehner, a Practical Theory of Programming, Springer-Verlag 1993. Most recent edition online at <a rel="nofollow" class="external text" href="https://www.cs.toronto.edu/~hehner/aPToP">a Practical Theory of Programming</a>.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="https://www.cs.toronto.edu/~hehner/publist.html">Publications</a> by <a href="Eric_Hehner" title="Eric Hehner">Eric Hehner</a>.</li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .asbox{position:relative;overflow:hidden}.mw-parser-output .asbox table{background:transparent}.mw-parser-output .asbox p{margin:0}.mw-parser-output .asbox p+p{margin-top:0.25em}.mw-parser-output .asbox-body{font-style:italic}.mw-parser-output .asbox-note{font-size:smaller}.mw-parser-output .asbox .navbar{position:absolute;top:-0.75em;right:1em;display:none}.mw-parser-output :not(p):not(.asbox)+style+.asbox,.mw-parser-output :not(p):not(.asbox)+link+.asbox{margin-top:3em}

/* end https://en.wikipedia.org/ */

</style></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-06-14" href="https://en.wikipedia.org/wiki/?title=Predicative_programming&oldid=1295483151">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>